ds:(IdType), da:(IdKndType), A, B:Type, X:Interface(ds;da;A), Y:Interface(ds;da;B), es:ES.
es-decl(es;ds;da)  (es-interface-left([[interface-union(X;Y)]]) = [[X]]  AbsInterface(A)) 

latex

Definitions

s ~ t, interface-union(X;Y), p q, in-interface(es;X;e), Knd, Id, <a, b>, f(a), f o g  , can-apply(f;x), do-apply(f;x), es-interface-left(X), P  Q, x:A. B(x), AbsInterface(A), [[X]], left + right, Top, E, t  T, s = t, es-decl(es;ds;da), ES, b, x:A  B(x), Interface(ds;da;A), a:A fp B(a), Type, x:AB(x), LocKnd, loc(e), kind(e), x  dom(f), SQType(T), {T}, , deq-member(eq;x;L), hasloc(k;i), t.1, {x:A| B(x)} , let x,y = A in B(x;y), type List, fpf-domain(f), x. t(x), x.A(x), let i,k:LocKnd = ik in P(i;k), x,y. t(x;y), locknd-deq(), as @ bs, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , , P  Q, (x  l), P  Q, P & Q, P  Q, t.2, (state when e), val(e), interface-val(es;X;e), f(x), Unit, outl(x), inl x , inr x , x:A.B(x), Void, ff, A, False

Lemmas

equal-top, interface-val wf, assert of bnot, eqff to assert, eqtt to assert, member append, l member wf, assert-deq-member, or functionality wrt iff, assert of bor, iff transitivity, deq-member wf, bor wf, append wf, locknd-deq wf, LocKnd wf, iff imp equal bool, top wf, locknd-spread wf2, fpf-trivial-subtype-top, fpf-domain wf, Knd wf, Id wf, hasloc wf, assert wf, es-hasloc, es-kind wf, es-loc wf, bool sq, abs-interface wf, interface-union wf, es-interface-left wf